Hiểu một cách chính thức thì lý thuyết kiểu nghiên cứu về hệ thống kiểu. Một ngôn ngữ lập trình phải có kiểm tra kiểu (type check) bằng cách sử dụng hệ thống kiểu cho dù ở thời gian biên dịch hay thời gian chạy, ghi chú thủ công hay tự động suy ra. Như Mark Manasse đã nói rõ rằng:[3]

Vấn đề cơ bản được chỉ ra bởi lý thuyết kiểu là để bảo đảm chương trình có ý nghĩa. Vấn đề cơ bản gây ra bởi lý thuyết kiểu là các chương trình có ý nghĩa có thể không có ý nghĩa vốn được gán cho chúng. Việc tìm kiếm hệ thống kiểu phong phú hơn là kết quả của sự căng thẳng này.

Cho dù là được tự động bởi trình biên dịch hay được đặc tả bởi lập trình viên, hệ thống kiểu sẽ khiến hành vi chương trình trở nên bất hợp pháp nếu nó nằm ngoài quy tắc hệ thống kiểu. Ưu điểm của hệ thống kiểu đặc tả bởi lập trình viên gồm:

• Trừu tượng hóa (abstraction) hay mô đun hóa (modularity) – Các kiểu cho phép lập trình viên suy nghĩ ở mức cao hơn mức bit hoặc byte mà không cần quan tâm đến hiện thực ở mức thấp hơn. Ví dụ, lập trình viên có thể bắt đầu nghĩ về chuỗi (string) như là một tập các giá trị kí tự thay vì một mảng các byte. Cao hơn một chút, kiểu cho phép lập trình viên nghĩ và thể hiện giao diện giữa hai hệ thống con với bất kì kích thước nào. Điều này cho phép nhiều mức độ địa phương hóa để các định nghĩa cần thiết cho tính tương hợp giữa các hệ thống con vẫn thống nhất khi hai hệ thống giao tiếp với nhau.
• Tài liệu hóa (documentation) – Trong các hệ thống kiểu lớn hơn, kiểu có thể đóng vai trò như tài liệu để làm rõ mục đích của lập trình viên. Ví dụ, nếu lập trình viên định nghĩa một hàm trả về kiểu thời gian (timestamp), nó ghi tài liệu hàm với kiểu thời gian được khai báo tường minh trong mã với kiểu số nguyên.

Ưu điểm của hệ thống kiểu đặc tả bởi trình biên dịch gồm:

• Tối ưu hóa (optimization) – Kiểm tra kiểu tĩnh có thể cung cấp thông tin thời gian biên dịch có ích. Ví duk, nếu một kiểu yêu cầu giá trị nằm trong bộ nhớ phải là bộ số của 4 byte, trình biên dịch có thể sử dụng lệnh máy hiệu quả hơn.
• An toàn (safety) – Một hệ thống kiểu cho phép trình biên dịch phát hiện mã vô nghĩa hay có thể là mã không phợp lệ. Ví dụ, chúng ta có thể xác định biểu thức 3 / "Hello, World" là không hợp lệ, vì các quy tắc không xác định được cách chia một số nguyên cho một chuỗi. Kiểu mạnh hường an toàn hơn, nhưng không thể bảo đảm an toàn kiểu (type safety) được.